00100	
00200	
00300	
00400	
00500	
00600	
00700	
00800	
00900	     An Application of Theorem - Proving Techniques to Puzzle - Solving
01000	
01100	
01200	
01300	
01400	
01500	
01600	
01700	
01800	
     

00100	
00200	
00300	In recent years much attention has been given to the question
00400	of applying theorem-proving techniques to areas other than formal
00500	mathematics.  These applications extend from the sometimes trivial representation of
00600	the problems in first-order formalism to the more sophisticated answer-
00700	extraction techniques used in question-answering.
00800	
00900	In this section we describe a different type of application -- the use 
00950	of the deductive section of the theorem prover as a subroutine to a puzzle-solving procedure.
01000	
01100	Consider the following well-known puzzle:
01200	
01300	St1.  There are five houses, each of a different color and inhabited
01400	by men of different nationalities, with different pets, drinks,
01500	and cigarettes.
01600	St2.  The Englishman lives in the red house.
01700	St3.  The Spaniard owns the dog.
01800	St4.  Coffee is drunk in the green house.
01900	St5.  The Ukranian drinks tee.
02000	St6.  The green house is immediately to the right of the ivory house.
02100	St7.  The Old Gold smoker owns snails.
02200	St8.  Kools are smoked in the yellow house.
02300	St9.  Milk is drunk in the middle house.
02400	St10. The Norwegian lives in the first house on the left.
02500	St11. The man who smokes Chesterfields lives in the house next to the man with the fox.
02600	St12. Kools are smoked in the house next to the house where the horse is kept.
02700	St13. The Lucky Strike smoker drinks orange jiuce.
02800	St14. The Japanese smokes Parliments.
02900	St15. The Norwegian lives next to the blue house.
03000	
03100	Q1. Who drinks water ?
03200	Q2. Who owns the Zebra ?
03300	
03400	
     

00100	
00200	A naiive first-order axiomatization of St.2 through St. 15 might be:
00300	
00400	A(x)eng(x) = red(x);
00500	A(x)span(x) = dog(x);
00600	A(x)coffee(x) = green(x);
00700	A(x)ukr(x) =  tea(x);
00800	ivory(1) = green(2); ivory(2) = green(3); ivory(3) = green(4); ivory(4) = green(5);
00900	A(x)oldg(x) = snails(x);
01000	A(x) kools(x) = yellow(x);
01100	milk(3);
01200	nor(1);
01300	A(x)A(y)(chest(x) & fox(y) > next (x,y));
01400	A(x)A(y)(kools(x) & horse(y) > next (x,y));
01500	A(x)lucky(x) = oj(x);
01600	A(x)jap(x) = parl(x);
01700	A(x)A(y)(nor(x1) & blue(x2) > next(x,y));
01800	
01900	To these we add simple axiomatization of  the NEXT relation.
02000	next(1,2); next(2,3); ...}next(1,3); }next(1,4); ...
02100	
02200	However to capture the intent of the first statement,St1., requires a large
02300	set of first-order statements expressing uniqueness and ******.
02400	Proceeding with such a formidable set of axioms did not seem
02500	profitable.  It is at least clear how St 1. is to be used:
02600	When we can assert that a specific property holds for an individual
02700	house, e.g. milk(3) then St1. tells us two things 1) milk is not
02800	drunk in any other house -- }milk(1); }milk(2); }milk(4); }milk(5);
02900	and it aso tells us that (2) no other beverage is consumed
03000	in the third house -- }water(3); ... etc.
03100	
03200	 It is  also clear that we could appeal to the on-line facilities,
03300	stopping the prover whenever such positive assertions as milk(3) )
03400	are deduced, and insert the appropriate consequences of St1.
03500	
03600	The reader should have noticed that  St1 has other uses than the one outlined
03700	above.  Namely if we have established that a paticular prperty does not
03800	hold for any four of the five houses,we can conclude by St1 that
03900	the property must hold for the remaining house.  Similarly,
04000	that if four of the five elements of one of the classes of properties do not
04100	hold for a specific house then the remaining member of the class must hold for that
04200	house.  This second application of St1 could also be accomplished on-line
04300	but requires more bookeeping by the user.  He must record and remember
04400	those deductions which exclude properties from being associated with particular
04500	houses.  When an appropriate set of four of these deductions arises then he can
04600	insert the appropriate the appripriate positive deduction.
04700	
04800	
04900	
05000	
05100	
05200	
     

00100	
00200	The program structure is clear:  Call upon the prover to establish the assertions
00300	of the form }P(x) and P(x), where P is an element of one of the classes
00400	of properties.  When such a deduction occurs, return to the calling program.
00500	Using the new assertion construct any new consequences of St1.
00600	Insert these statements into the list of clauses and call the prover
00700	with the augmented list of  clauses,making deductions until
00800	new unit clauses are asserted.
00900	Using this technique it is easy to establish that  the Norwegian
01000	drinks water.
01100	
01200	We require more of St1 to answer the second question -- who owns the
01300	Zebra.  Namely, that if we know }P1(x) and }P2(x), and }P3(x),
01400	we can assert P4(x) or P5(x) must hold.  Using this information we completed the
01500	puzzle.  Rather than announce the answer we leave it for the reader to discover.
01600